ds:x:Id fp Type, da:k:Knd fp Type, l: List, v:ecl-trans-tuple{i:l}(ds;da),
L:event-info(ds;da) List, n:.
ecl-trans-halt2(ds;da;ecl-add-catch(v;l))(n,L)

(n  l) & ecl-trans-halt2(ds;da;v)(n,L)  n = 0   & (ml.ecl-trans-halt2(ds;da;v)(m,L)) 

latex

Definitions

b, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-h(v), ecl-trans-type(A), ecl-trans-state-from(v;z;L), ecl-trans-init(v), ecl-trans-tuple{i:l}(ds;da), t  T, x:A. B(x), P  Q, Id, x. t(x), a:A fp B(a), Knd, , event-info(ds;da), ecl-trans-halt2(ds;da;A), ecl-trans-state(v;L), ecl-add-catch(A;l), (xL.P(x)), Prop, P & Q, (x  l), A, P  Q, P  Q, P  Q, false, , p  q, reduce(f;k;as), i=j, p  q, NatDeq, deq-member(eq;x;L), b

Lemmas

assert of bor, assert of bnot, not functionality wrt iff, assert-deq-member, iff transitivity, assert of band, assert of eq int, bnot wf, deq-member wf, nat-deq wf, band wf, eq int wf, iff functionality wrt iff, or functionality wrt iff, and functionality wrt iff, l exists reduce, reduce wf, bor wf, bool wf, bfalse wf, not wf, l member wf, l exists wf, assert wf, event-info wf, ecl-trans-tuple wf, nat wf, Knd wf, fpf wf, Id wf, ecl-trans-state wf, ecl-trans-type wf